В рассматриваемом здесь втором примере используется сколемизация и применяются выражения, которые не являются определенными. Это приводит к созданию немного более сложной структуры доказательства. На естественном языке эта задача формулируется, как описано ниже.

Каждого, кто любит всех животных, кто-то любит.

Любого, кто убивает животных, никто не любит.

Джек любит всех животных.

Кота по имени Тунец убил либо Джек, либо Любопытство.

Действительно ли этого кота убило Любопытство?

Рис. 9.7. Процедура доказательства с помощью резолюции того, что полковник Уэст совершил преступление

Вначале представим в логике первого порядка первоначальные высказывания, некоторые фоновые знания и отрицаемую цель G:

Затем применим процедуру преобразования, чтобы преобразовать каждое высказывание в форму CNF:

Доказательство с помощью метода резолюции того, что кота убило Любопытство, приведено на рис. 9.8. На естественном языке это доказательство может быть перефразировано, как показано ниже.

Предположим, что кота Тунца убило не Любопытство. Мы знаем, что это сделал либо Джек, либо Любопытство; в таком случае это должен был сделать Джек. Итак, Тунец — кот, а коты — животные, поэтому Тунец — животное. Любого, кто убивает животное, никто не любит, поэтому мы делаем вывод, что никто не любит Джека. С другой стороны, Джек любит всех животных, поэтому кто-то его любит; таким образом, возникает противоречие. Это означает, что кота убило Любопытство.

Рис. 9.8. Процедура доказательства с помощью резолюции того, что кота убило Любопытство. Обратите внимание на то, что при выводе выражения Loves (G (Mack;, Jack; использовалась факторизация